-- Submitted by
-- Dhasarathy Parthasarathy
-- Test cases for every problem Ai are functions of name testAixj
-- Every testcase testAixj has been run and the outputs have been verified. The generated outputs confirm the correctness of the descriptions
-- (in most cases)
import Lava
import Lava.Patterns
import Lava.Arithmetic
import EFile11
import DrawPP11

type Binary = [Bit]

--A1
-- verifies if two pairs of bits are equal
pairEqualityChecker :: ((Bit, Bit), (Bit, Bit)) -> Bit
pairEqualityChecker ((a,b),(c,d)) = and2(a<=>c,b<=>d)

-- exhaustive simulation of fullAdd1 and fullAdd using their 'domain' as inputs
-- expected output [high,high,high,high,high,high,high,high]
-- simulated and verified
verifyFullAdd1 = ok
	where
	outFullAdd1 = simulateSeq fullAdd1 domain
	outFullAdd = simulateSeq fullAdd domain
	ok = (simulateSeq pairEqualityChecker) (zipp(outFullAdd1,outFullAdd))
----------------------------------------------------------------------------------------------------------------------------------------------------	
--A2
-- property to check if outputs of 2 circuits are the same
propPairOPEquivalenceCheck circ1 circ2 a = ok
	where
	out1 = circ1 a
	out2 = circ2 a
	ok = pairEqualityChecker(out1,out2)

-- formal verification using the property above
-- expected output Valid,Valid
-- simulated and verified
formalVerifyFullAdd1SAT = satzoo (propPairOPEquivalenceCheck fullAdd1 fullAdd)
formalVerifyFullAdd1SMV = smv (propPairOPEquivalenceCheck fullAdd1 fullAdd)
----------------------------------------------------------------------------------------------------------------------------------------------------
--A3

-- property to check associativity of circ
propAssoc circ (a,b,c) = ok
	where
	out1 = circ(circ(a,b),c)
	out2 = circ(a,circ(b,c))
	ok = pairEqualityChecker(out1,out2)

-- formal verification of dotOp using the property above
-- expected output Valid,Valid
-- simulated and verified
formalVerifyDotOpAssociativeSAT = satzoo (propAssoc dotOp)
formalVerifyDotOpAssociativeSMV = smv (propAssoc dotOp)
----------------------------------------------------------------------------------------------------------------------------------------------------
--A4
-- function to check equality of a pair of (Binary,Bit) which is the adder output
adderOPEqualityChecker :: ((Binary,Bit),(Binary,Bit)) -> Bit
adderOPEqualityChecker ((as,a),(bs,b)) = and2(as<==>bs,a<=>b)

propAdderOPEquivalenceCheck circ1 circ2 a = ok
	where
	out1 = circ1 a
	out2 = circ2 a
	ok = adderOPEqualityChecker(out1,out2)

-- quantified property for formal verification
propAdderOPEquivalenceCheckForSizeN n a b = forAll (list n) $ \as -> propAdderOPEquivalenceCheck a b as

-- expected output Valid in all cases
-- simulated and verified
testA4x0 = satzoo (propAdderOPEquivalenceCheckForSizeN 2 adder0 adder6)
testA4x1 = satzoo (propAdderOPEquivalenceCheckForSizeN 4 adder0 adder6)
testA4x2 = satzoo (propAdderOPEquivalenceCheckForSizeN 8 adder0 adder6)
testA4x3 = satzoo (propAdderOPEquivalenceCheckForSizeN 16 adder0 adder6)
testA4x4 = satzoo (propAdderOPEquivalenceCheckForSizeN 32 adder0 adder6)

formalVerifyAdder0Adder6EqSAT = do
								testA4x0
								testA4x1
								testA4x2
								testA4x3
								testA4x4
----------------------------------------------------------------------------------------------------------------------------------------------------
--A5

-- adder where the pattern is a parameter
adder8 :: PP (Bit,Bit) -> [(Bit, Bit)] -> ([Bit], Bit)
adder8 pattern abs = (ss,cout)
  where
    gps            = map gpC abs
    (cs,cout)      = (pattern (mkFan dotOp) ->- unsnoc ->- (map fst -|- fst) ) gps
    ((_,p) : gps') = gps
    rs             = zip cs gps'
    ss             = p : map sumC rs

-- testing using ser and skl patterns
testA5x0 = satzoo (propAdderOPEquivalenceCheckForSizeN 4 (adder8 ser) adder6)
testA5x1 = satzoo (propAdderOPEquivalenceCheckForSizeN 4 (adder8 skl) adder7)

-- expected output Valid in all cases
-- simulated and verified
formalVerifyAdder8Adder6Adder7EqSAT = do
									  testA5x0
									  testA5x1
----------------------------------------------------------------------------------------------------------------------------------------------------
--A6

-- the row of operators at the top and bottom
wrapRowOperators :: PP a
wrapRowOperators f [] = []
wrapRowOperators f [a] = [a]
wrapRowOperators f (a:b:bs) = f[a,b] ++ (wrapRowOperators f bs)

-- the fan operator that is used for the prefix network
fanOfOperator :: PP a
fanOfOperator f as = outs
	where
	op1 = head as
	opList = tail as
	elts = [2*i | i<-[1..length as`div`2]] --[2*i | i<-[1..(nthRootOf2 1 (length as))]]
	ops = [opList!!(ind-1) | ind <- elts]
	(rx:result) = f (op1:ops)
	outs = putInList result elts opList
	
-- the prefix network
-- processes in pairs of 2,4,8... of inputs and recursively computes the sum
prefixNetwork :: Int -> PP a
prefixNetwork n f [] = []
prefixNetwork n f as | length as == 2 = as
prefixNetwork n f as = cs
	where
	(ls,rs) = splitAt (2*n) as
	(op1,x) = splitAt n ls
	ops2 = if length x > 2
		   then prefixNetwork 2 f x
		   else x
	outs = fanOfOperator f ([last op1] ++ ops2)
	newLs = op1 ++ outs
	newRs = if length rs < (2*n)
			then fanOfOperator f ([last newLs] ++ prefixNetwork 2 f rs)
			else rs
	cs = if length rs < (2*n)
		 then newLs ++ newRs
		 else prefixNetwork (2*n) f (newLs++newRs)

-- bKung 2 block pattern using the functions above
bKung :: PP a
bKung f [a] = [a]
bKung f as  = out
	where
	xs = wrapRowOperators f as
	(out0:ys) = prefixNetwork 2 f xs
	out = out0:(wrapRowOperators f ys)

-- my basic method for testing was to run the pattern with 'pplus' and n 1s and see if the output is 1 to n
-- this holds for any n
basicTestbKung n = simulate (bKung pplus) (replicate n 1)

-- basic check of the pattern for different sizes
-- expected output True in all cases
-- simulated and verified
testA6x0 = check bKung 8
testA6x1 = check bKung 16
testA6x2 = check bKung 32
testA6x3 = check bKung 64

basicCheckTestbKPattern = [testA6x0,testA6x1,testA6x2,testA6x3]

-- a fast adder built using bKung pattern for formal verification
bKungFastAdder :: [(Bit, Bit)] -> ([Bit], Bit)
bKungFastAdder abs = adder8 bKung abs

-- formal verification of bKungFastAdder for different sizes
-- expected output Valid in all cases
-- simulated and verified
testA6x4 = satzoo (propAdderOPEquivalenceCheckForSizeN 8 bKungFastAdder adder6)
testA6x5 = satzoo (propAdderOPEquivalenceCheckForSizeN 16 bKungFastAdder adder6)
testA6x6 = satzoo (propAdderOPEquivalenceCheckForSizeN 32 bKungFastAdder adder6)
testA6x7 = satzoo (propAdderOPEquivalenceCheckForSizeN 64 bKungFastAdder adder6)

formalVerificationBKFastAdder = do
								testA6x4
								testA6x5
								testA6x6
								testA6x7

-- depth test of the bKung pattern		
depthTest n = simulate (bKung delFan)(replicate n 0)

-- Not sure about the expected outputs for the larger sizes
-- calculated the delay for 8, it doesn't match with the output [1,2,2,3,3,4,4,3]
-- but delFan is implemented such that the delay for the 1st element is 1
-- so I think my implementation is not compatible with delFan
testA6x8 = depthTest 8
testA6x9 = depthTest 16
testA6x10 = depthTest 32

depthTestbKPattern = [testA6x8,testA6x9,testA6x10]
----------------------------------------------------------------------------------------------------------------------------------------------------
-- A7

-- the operator to calculate the number of operations
opCount ::  (Signal Int, Signal Int) -> Signal Int
opCount (a,b) = (1+minimum[a,b])

-- takes a pattern and size and gives the number of operators
opCountCheck pp n = simulate ((pp (mkFan opCount))->- sum) (replicate n 0)

-- got the expected output for serial sklansky(from the fig in the questions) and bKung patterns
-- [11,27,80,192,31,63]
-- takes a pattern and size and gives the number of operators
testA7x0 = opCountCheck bKung 8
testA7x1 = opCountCheck bKung 16

testA7x2 = opCountCheck skl 32
testA7x3 = opCountCheck skl 64

testA7x4 = opCountCheck ser 32
testA7x5 = opCountCheck ser 64

opCountTest = [testA7x0,testA7x1,testA7x2,testA7x3,testA7x4,testA7x5]
----------------------------------------------------------------------------------------------------------------------------------------------------
-- A8
-- starts with a big collection of helper functions

-- takes a list of indices and elements and replaces the elements of another list in the given indices 
putInList :: [a] -> [Int] -> [a] -> [a]
putInList [] [] as = as
putInList [] i as = as
putInList (e:els) (i:is) as = out
	where
	(ls,rs) = splitAt (i) as
	newLs = (init ls) ++ [e]
	out = if null els
		  then newLs ++ rs
		  else putInList els is (newLs ++ rs)

-- used in the function above
-- weeds out indices that are outside the list		  
sanitizeList :: [Int]->Int->[Int]
sanitizeList [] len = []
sanitizeList elts len = out
	where
	out = if (last elts) <= len
		  then elts
		  else sanitizeList (init elts) len

joinLists :: [[a]] -> [a]
joinLists [] = []
joinLists (aa:aas) = aa ++ joinLists(aas)

nthPowerOf :: Int -> Int -> Int -> Int
nthPowerOf i num base = out
	where
	out = if num`div`base == 1
		  then i
		  else nthPowerOf (i+1) (num`div`base) base		  
	
-- to calculate the 'root' of the network
serialrootCalc :: Int->Int->Int->Int
serialrootCalc i k l = root
	where
	root = if i*k >= l
		   then i*k
		   else serialrootCalc (i*k) k l

-- the serial prefix operator
-- applies (ser f) to a list 
serialPrefixOperator :: Int -> Int -> PP a
serialPrefixOperator root block f [] = []
serialPrefixOperator root block f as = outs
	where
	elts = [i*(root `div` block) | i<-[1..block]]
	sanElts = sanitizeList elts (length as)
	ops = if null sanElts
		  then []
		  else [as!!(ind-1) | ind <- sanElts]
	results = ser f (ops)
	outs = putInList results elts as

-- the serial prefix network
-- calculates the prefix sums recursively from the root, the root is the largest nth power of the block size
serialPrefixNetwork :: Int -> Int -> PP a
serialPrefixNetwork root block f [] = []
serialPrefixNetwork root block f as = out
	where
	splits = if root == block
			 then []
			 else chop (root`div`block) as
	lowerResults = if root == block
				   then [serialPrefixOperator root block f as]
				   else [serialPrefixNetwork (root`div`block) block f i | i <- splits]
	out = if root == block
		  then head(lowerResults)
	      else serialPrefixOperator root block f (joinLists lowerResults)

-- the fan analog of the serialPrefixOperator
fanPrefixOperator :: Int -> Int -> PP a
fanPrefixOperator root block f [] = []
fanPrefixOperator root block f as = outs
	where
	op1 = head as
	opList = tail as
	elts = [i*(root`div`block) | i<-[1..block-1]]
	sanElts = sanitizeList elts (length opList)
	ops = [opList!!(ind-1) | ind <- sanElts]
	(rx:results) = f (op1:ops)
	outs = putInList results elts opList

-- the fan prefix network
-- calculates the prefix sums row by row from the same root

fanPrefixNetwork :: Int -> Int -> PP a
fanPrefixNetwork root block f as = out
	where
	splits = chop (root) as
	results = [fanPrefixOperator root block f (last(splits!!(i-1)):splits!!(i)) | i<-[1..(length splits - 1)]]
	out = if root == block
		  then splits!!0 ++ joinLists results
		  else fanPrefixNetwork (root`div`block) block f (splits!!0 ++ joinLists results)

-- the bKungG pattern
-- here k is both the block width and fanout
bKungG :: Int -> PP a
bKungG k f as | length as < k = as
bKungG k f as = ys
	where
	root = serialrootCalc 1 k (length as)
	xs = serialPrefixNetwork root k f as
	ys = fanPrefixNetwork root k f xs

-- basic testing done in a similar way explained in bKung by an input of n ones and checking if the outputs are 1 to n
-- as far as i tested, the expected value is generated for any k and n
basicTestbKungG k n = simulate(bKungG k pplus) (replicate n 1)

-- verification by building a fast adder using bKungG
bKungGFastAdder :: Int -> [(Bit, Bit)] -> ([Bit], Bit)
bKungGFastAdder k abs = adder8 (bKungG k) abs

-- a random selection of input size and block size
-- tested for a wide variety of combinations and got Valid as output, a few tests are here
testA8x0 = satzoo (propAdderOPEquivalenceCheckForSizeN 8 (bKungGFastAdder 2) adder6)
testA8x1 = satzoo (propAdderOPEquivalenceCheckForSizeN 16 (bKungGFastAdder 3) adder6)
testA8x2 = satzoo (propAdderOPEquivalenceCheckForSizeN 32 (bKungGFastAdder 4) adder6)
testA8x3 = satzoo (propAdderOPEquivalenceCheckForSizeN 64 (bKungGFastAdder 5) adder6)

formalVerifbKungGFastadder = do
							 testA8x0
							 testA8x1
							 testA8x2
							 testA8x3
----------------------------------------------------------------------------------------------------------------------------------------------------
--A9 
-- the serial prefix operator from bKungG with the pattern as a parameter
serialPrefixOperatorG :: Int -> Int -> PP a -> PP a
serialPrefixOperatorG root block pp f [] = []
serialPrefixOperatorG root block pp f as = outs
	where
	elts = [i*(root `div` block) | i<-[1..block]]
	sanElts = sanitizeList elts (length as)
	ops = if null sanElts
		  then []
		  else [as!!(ind-1) | ind <- sanElts]
	results = pp f (ops)
	outs = putInList results elts as

serialPrefixNetworkG :: Int -> Int -> PP a -> PP a
serialPrefixNetworkG root block pp f [] = []
serialPrefixNetworkG root block pp f as = out
	where
	splits = if root == block
			 then []
			 else chop (root`div`block) as
	lowerResults = if root == block
				   then [serialPrefixOperatorG root block pp f as]
				   else [serialPrefixNetworkG (root`div`block) block pp f i | i <- splits]
	out = if root == block
		  then head(lowerResults)
	      else serialPrefixOperatorG root block pp f (joinLists lowerResults)
		  
-- the bKungG network along with a pattern as a parameter
bKungG1 :: Int -> PP a -> PP a
bKungG1 k pp f as | length as < k = as
bKungG1 k pp f as= ys
	where
	root = serialrootCalc 1 k (length as)
	xs = serialPrefixNetworkG root k pp f as
	ys = fanPrefixNetwork root k f xs
	
-- verification by building a fast adder using bKungG1
-- using a serial input pattern
bKungG1SerAdder :: Int -> [(Bit, Bit)] -> ([Bit], Bit)
bKungG1SerAdder k abs = adder8 (bKungG1 k ser) abs

testA9x0 = satzoo (propAdderOPEquivalenceCheckForSizeN 14 (bKungG1SerAdder 2) adder6)
testA9x1 = satzoo (propAdderOPEquivalenceCheckForSizeN 25 (bKungG1SerAdder 3) adder6)

-- using a sklansky input pattern
bKungG1SklAdder :: Int -> [(Bit, Bit)] -> ([Bit], Bit)
bKungG1SklAdder k abs = adder8 (bKungG1 k skl) abs

testA9x2 = satzoo (propAdderOPEquivalenceCheckForSizeN 64 (bKungG1SklAdder 2) adder6)
testA9x3 = satzoo (propAdderOPEquivalenceCheckForSizeN 64 (bKungG1SklAdder 4) adder6)
testA9x4 = satzoo (propAdderOPEquivalenceCheckForSizeN 64 (bKungG1SklAdder 5) adder6)

formalVerifbKungG1Pattern = do
							testA9x0
							testA9x1
							testA9x2
							testA9x3
							testA9x4
----------------------------------------------------------------------------------------------------------------------------------------------------
--A10

-- to calculate the delay of the general network of size 64
-- depending upon the prefix pattern and block size
delayCalc k pp = (bKungG1 k pp delFan)(replicate 64 0)
delayOf64BitPPN k pp = simulate maximum (delayCalc k pp)

-- to calculate the number of operators for the same parameters
opCountCalc k pp = (bKungG1 k pp (mkFan opCount))(replicate 64 0)
numOpsOf64BitPPN k pp = simulate sum (opCountCalc k pp)

-- sequentially calculates the delay and operator count for different block sizes
-- this function is for the case of the serial prefix pattern
sequenceCalcSer :: Int -> [(Signal Int,Signal Int)]
sequenceCalcSer i = as
	where
	adel = (delayOf64BitPPN i ser)
	anOP = (numOpsOf64BitPPN i ser)
	as = if i >= 64
		 then [(adel,anOP)]
		 else [(adel,anOP)] ++ sequenceCalcSer (i+1)

-- this function is for the case of the sklansky prefix pattern
sequenceCalcSkl :: Int -> [(Signal Int,Signal Int)]
sequenceCalcSkl i = as
	where
	adel = (delayOf64BitPPN i skl)
	anOP = (numOpsOf64BitPPN i skl)
	as = if i >= 64
		 then [(adel,anOP)]
		 else [(adel,anOP)] ++ sequenceCalcSkl (i+1)

testA10x0 = sequenceCalcSer 4
testA10x1 = sequenceCalcSkl 4

-- when compared between serial and sklansky networks, the serial network delays are too high for fast addition
-- in the case of sklansky networks, the number of operators is much higher
-- when compared between the two the sklansky block 5 combination is reasonable, though there are huge differences in delay
-- number of operators when compared to its serial counterpart, the sklansky 5 block presents more gain than the sklansky
-- networks of other block sizes. The same concept can be extended to other basic prefix patterns
size64TradeOffAdder :: PP a
size64TradeOffAdder f as = (bKungG1 5 skl f) as
----------------------------------------------------------------------------------------------------------------------------------------------------